wneuper/isa: test/Tools/isac/Test_Theory.thy@b7a2ad3b3d45 (annotated)

wneuper@59119	1	(* use this theory for tests before Build_Isac.thy has succeeded *)
Walther@60576	2	theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"
neuper@52102	3	begin
wenzelm@60192	4	ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
Walther@60571	5	(* ATTENTION: tests with Test_Code.init_calc, CalcTree @{context} do NOT work here, because Thy_Info.get_theory
wenzelm@60217	6	requires session Isac, see $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory *)
neuper@52102	7
wneuper@59472	8	section \<open>code for copy & paste ===============================================================\<close>
wneuper@59472	9	ML \<open>
walther@59686	10	"~~~~~ fun xxx , args:"; val () = ();
walther@59686	11	"~~~~~ and xxx , args:"; val () = ();
Walther@60576	12	"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
Walther@60576	13	"~~~~~ continue fun xxx"; val () = ();
Walther@60576	14	(if) (then); (else); (case) (of); (return value); (in) (end);
walther@59686	15	"xx"
Walther@60629	16	^ "xxx" (+) (+++) (keep for continuing YYYYY) (isa) (isa2) (**)
Walther@60576	17	\<close> ML \<open> (//----------- adhoc inserted n ----------------------------------------------------\\)
Walther@60627	18	(//------------------ adhoc inserted n ----------------------------------------------------\\)
Walther@60576	19	(\\------------------ adhoc inserted n ----------------------------------------------------//)
Walther@60576	20	\<close> ML \<open> (\\----------- adhoc inserted n ----------------------------------------------------//)
Walther@60576	21
Walther@60576	22	\<close> ML \<open> (//----------- step into XXXXX -----------------------------------------------------\\)
Walther@60576	23	(//------------------ step into XXXXX -----------------------------------------------------\\)
Walther@60629	24	(keep for continuing YYYYY)
Walther@60578	25	\<close> ML \<open> (------------- continuing XXXXX ------------------------------------------------------)
Walther@60578	26	(-------------------- continuing XXXXX ------------------------------------------------------)
Walther@60629	27	(kept for continuing YYYYY)
Walther@60576	28	(-------------------- stop step into XXXXX --------------------------------------------------)
Walther@60576	29	\<close> ML \<open> (------------- stop step into XXXXX --------------------------------------------------)
Walther@60576	30	(\\------------------ step into XXXXX -----------------------------------------------------//)
Walther@60576	31	\<close> ML \<open> (\\----------- step into XXXXX -----------------------------------------------------//)
Walther@60576	32
Walther@60576	33	(/------------------- check entry to XXXXX -------------------------------------------------\)
Walther@60576	34	(\------------------- check entry to XXXXX -------------------------------------------------/)
Walther@60576	35	(/------------------- check within XXXXX ---------------------------------------------------\)
Walther@60576	36	(\------------------- check within XXXXX ---------------------------------------------------/)
Walther@60576	37	(/------------------- check result of XXXXX ------------------------------------------------\)
Walther@60576	38	(\------------------- check result of XXXXX ------------------------------------------------/)
Walther@60576	39	(* final test ... ----------------------------------------------------------------------------*)
Walther@60576	40
Walther@60576	41	\<close> ML \<open> (//----------- inserted hidden code ------------------------------------------------\\)
Walther@60576	42	(//------------------ inserted hidden code ------------------------------------------------\\)
Walther@60576	43	(\\------------------ inserted hidden code ------------------------------------------------//)
Walther@60576	44	\<close> ML \<open> (\\----------- inserted hidden code ------------------------------------------------//)
Walther@60576	45
Walther@60576	46	\<close> ML \<open> (//----------- build new fun XXXXX -------------------------------------------------\\)
Walther@60576	47	(//------------------ build new fun XXXXX -------------------------------------------------\\)
Walther@60576	48	(\\------------------ build new fun XXXXX -------------------------------------------------//)
Walther@60576	49	\<close> ML \<open> (\\----------- build new fun XXXXX -------------------------------------------------//)
walther@59686	50	\<close> ML \<open>
wneuper@59472	51	\<close>
walther@59723	52	ML \<open>
walther@59723	53	\<close> ML \<open>
walther@59723	54	\<close> ML \<open>
walther@59723	55	\<close>
wneuper@59472	56	text \<open>
neuper@52102	57	declare [[show_types]]
neuper@52102	58	declare [[show_sorts]]
neuper@52102	59	find_theorems "?a <= ?a"
neuper@52102	60
Walther@60576	61	print_theorems
neuper@52102	62	print_facts
neuper@52102	63	print_statement ""
neuper@52102	64	print_theory
Walther@60576	65	ML_command \<open>Pretty.writeln prt\<close>
Walther@60576	66	declare [[ML_print_depth = 999]]
Walther@60576	67	declare [[ML_exception_trace]]
wneuper@59472	68	\<close>
neuper@52102	69
wneuper@59472	70	section \<open>=================================================================\<close>
wneuper@59472	71	ML \<open>
wneuper@59472	72	\<close> ML \<open>
wneuper@59472	73	\<close> ML \<open>
wneuper@59472	74	\<close> ML \<open>
wneuper@59472	75	\<close> ML \<open>
wneuper@59472	76	\<close> ML \<open>
wneuper@59472	77	\<close> ML \<open>
wneuper@59472	78	\<close>
walther@60152	79
Walther@60651	80	section \<open>=========="Minisubpbl/100-init-rootpbl.sml"========================================\<close>
Walther@60578	81	ML \<open>
Walther@60578	82	\<close> ML \<open>
Walther@60578	83	\<close> ML \<open>
Walther@60578	84	\<close> ML \<open>
Walther@60578	85	\<close> ML \<open>
Walther@60578	86	\<close> ML \<open>
Walther@60578	87	\<close> ML \<open>
Walther@60578	88	\<close>
Walther@60578	89
Walther@60578	90	section \<open>=================================================================\<close>
Walther@60576	91	ML \<open>
Walther@60576	92	\<close> ML \<open>
Walther@60576	93	\<close> ML \<open>
Walther@60576	94	\<close> ML \<open>
Walther@60576	95	\<close> ML \<open>
Walther@60576	96	\<close> ML \<open>
Walther@60576	97	\<close> ML \<open>
Walther@60576	98	\<close>
Walther@60576	99
wneuper@59472	100	section \<open>=================================================================\<close>
wneuper@59472	101	ML \<open>
wneuper@59472	102	\<close> ML \<open>
wneuper@59472	103	\<close> ML \<open>
wneuper@59472	104	\<close> ML \<open>
wneuper@59472	105	\<close> ML \<open>
wneuper@59472	106	\<close> ML \<open>
wneuper@59472	107	\<close> ML \<open>
wneuper@59472	108	\<close> ML \<open>
wneuper@59472	109	\<close>
neuper@52102	110
Walther@60576	111	section \<open>code for copy & paste ===============================================================\<close>
Walther@60576	112	ML \<open>
Walther@60576	113	"~~~~~ fun xxx , args:"; val () = ();
Walther@60576	114	"~~~~~ and xxx , args:"; val () = ();
Walther@60576	115	"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
Walther@60578	116	"~~~~~ continue fun xxx"; val () = ();
Walther@60576	117	(if) (then); (else); (case) (of); (return value); (in) (end);
Walther@60576	118	"xx"
Walther@60629	119	^ "xxx" (+) (+++) (keep for continuing YYYYY) (isa) (isa2) (**)
Walther@60576	120	\<close> ML \<open> (//----------- adhoc inserted n ----------------------------------------------------\\)
Walther@60576	121	(//----------------- adhoc inserted n ----------------------------------------------------\\)
Walther@60576	122	(\\------------------ adhoc inserted n ----------------------------------------------------//)
Walther@60576	123	\<close> ML \<open> (\\----------- adhoc inserted n ----------------------------------------------------//)
Walther@60576	124
Walther@60576	125	\<close> ML \<open> (//----------- step into XXXXX -----------------------------------------------------\\)
Walther@60576	126	(//------------------ step into XXXXX -----------------------------------------------------\\)
Walther@60629	127	(keep for continuing YYYYY)
Walther@60578	128	\<close> ML \<open> (------------- continuing XXXXX ------------------------------------------------------)
Walther@60578	129	(-------------------- continuing XXXXX ------------------------------------------------------)
Walther@60578	130	(kept for continuing XXXXX)
Walther@60576	131	(-------------------- stop step into XXXXX --------------------------------------------------)
Walther@60576	132	\<close> ML \<open> (------------- stop step into XXXXX --------------------------------------------------)
Walther@60576	133	(\\------------------ step into XXXXX -----------------------------------------------------//)
Walther@60576	134	\<close> ML \<open> (\\----------- step into XXXXX -----------------------------------------------------//)
Walther@60576	135
Walther@60578	136	(/------------------- check entry to XXXXX -------------------------------------------------\)
Walther@60578	137	(\------------------- check entry to XXXXX -------------------------------------------------/)
Walther@60578	138	(/------------------- check within XXXXX ---------------------------------------------------\)
Walther@60578	139	(\------------------- check within XXXXX ---------------------------------------------------/)
Walther@60578	140	(/------------------- check result of XXXXX ------------------------------------------------\)
Walther@60578	141	(\------------------- check result of XXXXX ------------------------------------------------/)
Walther@60578	142	(* final test ... ----------------------------------------------------------------------------*)
Walther@60578	143
Walther@60578	144	\<close> ML \<open> (//----------- inserted hidden code ------------------------------------------------\\)
Walther@60578	145	(//------------------ inserted hidden code ------------------------------------------------\\)
Walther@60578	146	(\\------------------ inserted hidden code ------------------------------------------------//)
Walther@60578	147	\<close> ML \<open> (\\----------- inserted hidden code ------------------------------------------------//)
Walther@60578	148
Walther@60576	149	\<close> ML \<open> (//----------- build new fun XXXXX -------------------------------------------------\\)
Walther@60576	150	(//------------------ build new fun XXXXX -------------------------------------------------\\)
Walther@60576	151	(\\------------------ build new fun XXXXX -------------------------------------------------//)
Walther@60576	152	\<close> ML \<open> (\\----------- build new fun XXXXX -------------------------------------------------//)
Walther@60576	153	\<close>
neuper@52102	154	end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 25 Jan 2023 15:52:33 +0100
changeset 60651	b7a2ad3b3d45
parent 60629	20c3d272d79c
child 60658	1c089105f581
permissions	-rw-r--r--