equal
deleted
inserted
replaced
1 theory Base_Tools |
1 theory Base_Tools |
2 imports Interpret.Interpret "../BridgeLibisabelle/BridgeLibisabelle" |
2 imports Interpret.Interpret |
3 (* ^^^ for KEStore_Elems.add_thes *) |
3 (** )"../BridgeJEdit/BridgeJEdit" ( *activate after devel.of BridgeJEdit*) |
|
4 (**) "../BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*) |
|
5 (* ^^^ for KEStore_Elems.add_thes *) |
4 begin |
6 begin |
5 subsection \<open>theorems for Base_Tools\<close> |
7 subsection \<open>theorems for Base_Tools\<close> |
6 axiomatization where (*for evaluating the assumptions of conditional rules*) |
8 axiomatization where (*for evaluating the assumptions of conditional rules*) |
7 |
9 |
8 (*last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*) |
10 (*last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*) |